text:
module Lens.Valid

import Data.List
import Data.Maybe
import Lens
import Lens.Uninhabited
import Lens.Util
import Map

%default total

make_preserves_validity : (k : Kind) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (Make k) s = Just s' -> transform_value (Make k) v = v' ->
    validate s v = True -> validate s' v' = True
make_preserves_validity KNull _ _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SNull SNull _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SNull SBoolean _ _ _ prf1 _ = rewrite sym prf1 in Refl
make_preserves_validity (KPrimitive KBoolean) SNull SNumber _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SNull SText _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SNull (SArray _ _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KBoolean) SNull (SObject _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KBoolean) SBoolean _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SNumber _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) SText _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) (SArray _ _) _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KBoolean) (SObject _) _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SNull SNull _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SNull SBoolean _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SNull SNumber _ _ _ prf1 _ = rewrite sym prf1 in Refl
make_preserves_validity (KPrimitive KNumber) SNull SText _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SNull (SArray _ _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KNumber) SNull (SObject _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KNumber) SBoolean _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SNumber _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) SText _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) (SArray _ _) _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KNumber) (SObject _) _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SNull SNull _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SNull SBoolean _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SNull SNumber _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SNull SText _ _ _ prf1 _ = rewrite sym prf1 in Refl
make_preserves_validity (KPrimitive KText) SNull (SArray _ _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KText) SNull (SObject _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity (KPrimitive KText) SBoolean _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SNumber _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) SText _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) (SArray _ _) _ _ _ Refl _ _ impossible
make_preserves_validity (KPrimitive KText) (SObject _) _ _ _ Refl _ _ impossible
make_preserves_validity KArray SNull SNull _ _ Refl _ _ impossible
make_preserves_validity KArray SNull SBoolean _ _ Refl _ _ impossible
make_preserves_validity KArray SNull SNumber _ _ Refl _ _ impossible
make_preserves_validity KArray SNull SText _ _ Refl _ _ impossible
make_preserves_validity KArray SNull (SArray False _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity KArray SNull (SArray True _) _ _ _ prf1 _ = rewrite sym prf1 in Refl
make_preserves_validity KArray SNull (SObject _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity KArray SBoolean _ _ _ Refl _ _ impossible
make_preserves_validity KArray SNumber _ _ _ Refl _ _ impossible
make_preserves_validity KArray SText _ _ _ Refl _ _ impossible
make_preserves_validity KArray (SArray _ _) _ _ _ Refl _ _ impossible
make_preserves_validity KArray (SObject _) _ _ _ Refl _ _ impossible
make_preserves_validity KObject SNull SNull _ _ Refl _ _ impossible
make_preserves_validity KObject SNull SBoolean _ _ Refl _ _ impossible
make_preserves_validity KObject SNull SNumber _ _ Refl _ _ impossible
make_preserves_validity KObject SNull SText _ _ Refl _ _ impossible
make_preserves_validity KObject SNull (SArray _ _) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity KObject SNull (SObject Empty) _ _ _ prf1 _ = rewrite sym prf1 in Refl
make_preserves_validity KObject SNull (SObject (Update _ _ _)) _ _ prf _ _ = absurd $ justInjective prf
make_preserves_validity KObject SBoolean _ _ _ Refl _ _ impossible
make_preserves_validity KObject SNumber _ _ _ Refl _ _ impossible
make_preserves_validity KObject SText _ _ _ Refl _ _ impossible
make_preserves_validity KObject (SArray _ _) _ _ _ Refl _ _ impossible
make_preserves_validity KObject (SObject _) _ _ _ Refl _ _ impossible

destroy_preserves_validity : (k : Kind) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (Destroy k) s = Just s' -> transform_value (Destroy k) v = v' ->
    validate s v = True -> validate s' v' = True
destroy_preserves_validity KNull _ _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KBoolean) SNull _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KBoolean) SBoolean SNull _ _ Refl prf1 _ = rewrite sym prf1 in Refl
destroy_preserves_validity (KPrimitive KBoolean) SNumber _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KBoolean) SText _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KBoolean) (SArray _ _) _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KBoolean) (SObject _) _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KNumber) SNull _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KNumber) SBoolean _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KNumber) SNumber SNull _ _ Refl prf1 _ = rewrite sym prf1 in Refl
destroy_preserves_validity (KPrimitive KNumber) SText _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KNumber) (SArray _ _) _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KNumber) (SObject _) _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KText) SNull _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KText) SBoolean _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KText) SNumber _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KText) SText SNull _ _ Refl prf1 prf2 = rewrite sym prf1 in Refl
destroy_preserves_validity (KPrimitive KText) (SArray _ _) _ _ _ Refl _ _ impossible
destroy_preserves_validity (KPrimitive KText) (SObject _) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray SNull _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray SBoolean _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray SNumber _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray SText _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray False _) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray True SNull) SNull _ _ Refl prf1 _ = rewrite sym prf1 in Refl
destroy_preserves_validity KArray (SArray True SBoolean) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray True SNumber) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray True SText) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray True (SArray _ _)) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SArray True (SObject _)) _ _ _ Refl _ _ impossible
destroy_preserves_validity KArray (SObject _) _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject SNull _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject SBoolean _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject SNumber _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject SText _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject (SArray _ _) _ _ _ Refl _ _ impossible
destroy_preserves_validity KObject (SObject Empty) SNull _ _ Refl prf1 _ = rewrite sym prf1 in Refl
destroy_preserves_validity KObject (SObject (Update _ _ _)) _ _ _ Refl _ _ impossible

add_property_preserves_validity : (k : Key) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (AddProperty k) s = Just s' -> transform_value (AddProperty k) v = v' ->
    validate s v = True -> validate s' v' = True
add_property_preserves_validity _ SNull _ _ _ Refl _ _ impossible
add_property_preserves_validity _ SBoolean _ _ _ Refl _ _ impossible
add_property_preserves_validity _ SNumber _ _ _ Refl _ _ impossible
add_property_preserves_validity _ SText _ _ _ Refl _ _ impossible
add_property_preserves_validity _ (SArray _ _) _ _ _ Refl _ _ impossible
add_property_preserves_validity k (SObject m) s' v v' prf prf1 prf2 with (get k m) proof prf3
    add_property_preserves_validity k (SObject _) _ _ _ prf _ _ | (Just _) = absurd $ prf
    add_property_preserves_validity k (SObject _) _ Null _ _ _ prf2 | Nothing = absurd $ prf2
    add_property_preserves_validity k (SObject _) _ (Primitive _) _ _ _ prf2 | Nothing = absurd $ prf2
    add_property_preserves_validity k (SObject _) _ (Array _) _ _ _ prf2 | Nothing = absurd $ prf2
    add_property_preserves_validity k (SObject sm) s' (Object vm) v' prf prf1 prf2 | Nothing =
        rewrite sym $ justInjective prf in
        rewrite sym prf1 in
        let
            split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
            exist = half_keys_eq_insert sm vm k SNull Null (fst split)
            valid = validate_properties_after_insert vm sm k Null SNull Refl (snd split)
        in rewrite exist in rewrite valid in Refl

remove_property_preserves_validity : (k : Key) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (RemoveProperty k) s = Just s' -> transform_value (RemoveProperty k) v = v' ->
    validate s v = True -> validate s' v' = True
remove_property_preserves_validity _ SNull _ _ _ Refl _ _ impossible
remove_property_preserves_validity _ SBoolean _ _ _ Refl _ _ impossible
remove_property_preserves_validity _ SNumber _ _ _ Refl _ _ impossible
remove_property_preserves_validity _ SText _ _ _ Refl _ _ impossible
remove_property_preserves_validity _ (SArray _ _) _ _ _ Refl _ _ impossible
remove_property_preserves_validity k (SObject m) s' v v' prf prf1 prf2 with (get k m) proof prf3
    remove_property_preserves_validity _ (SObject _) _ _ _ prf _ _ | Nothing = absurd $ prf
    remove_property_preserves_validity _ (SObject _) _ Null _ _ _ prf2 | (Just _) = absurd $ prf2
    remove_property_preserves_validity _ (SObject _) _ (Primitive _) _ _ _ prf2 | (Just _) = absurd $ prf2
    remove_property_preserves_validity _ (SObject _) _ (Array _) _ _ _ prf2 | (Just _) = absurd $ prf2
    remove_property_preserves_validity _ (SObject _) _ (Object _) _ prf _ _ | (Just SBoolean) = absurd $ prf
    remove_property_preserves_validity _ (SObject _) _ (Object _) _ prf _ _ | (Just SNumber) = absurd $ prf
    remove_property_preserves_validity _ (SObject _) _ (Object _) _ prf _ _ | (Just SText) = absurd $ prf
    remove_property_preserves_validity _ (SObject _) _ (Object _) _ prf _ _ | (Just (SArray _ _)) = absurd $ prf
    remove_property_preserves_validity _ (SObject _) _ (Object _) _ prf _ _ | (Just (SObject _)) = absurd $ prf
    remove_property_preserves_validity k (SObject sm) s' (Object vm) v' prf prf1 prf2 | (Just SNull) =
        rewrite sym $ justInjective prf in
        rewrite sym prf1 in
        let
            split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
            exist = half_keys_eq_remove sm vm k (fst split)
            valid = validate_properties_after_remove vm sm k (snd split)
        in rewrite exist in rewrite valid in Refl

rename_property_preserves_validity : (k, k' : Key) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (RenameProperty k k') s = Just s' -> transform_value (RenameProperty k k') v = v' ->
    validate s v = True -> validate s' v' = True
rename_property_preserves_validity _ _ SNull _ _ _ Refl _ _ impossible
rename_property_preserves_validity _ _ SBoolean _ _ _ Refl _ _ impossible
rename_property_preserves_validity _ _ SNumber _ _ _ Refl _ _ impossible
rename_property_preserves_validity _ _ SText _ _ _ Refl _ _ impossible
rename_property_preserves_validity _ _ (SArray _ _) _ _ _ Refl _ _ impossible
rename_property_preserves_validity k k' (SObject sm) s' v v' prf prf1 prf2 with (get k sm, get k' sm) proof prf3
    rename_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Nothing, _) = absurd $ prf
    rename_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just _) = absurd $ prf
    rename_property_preserves_validity _ _ (SObject _) _ Null _ _ _ prf2 | (Just _, Nothing) = absurd $ prf2
    rename_property_preserves_validity _ _ (SObject _) _ (Primitive _) _ _ _ prf2 | (Just _, Nothing) = absurd $ prf2
    rename_property_preserves_validity _ _ (SObject _) _ (Array _) _ _ _ prf2 | (Just _, Nothing) = absurd $ prf2
    rename_property_preserves_validity k k' (SObject sm) _ (Object vm) _ prf prf1 prf2 | (Just ksm, Nothing) with (get k vm) proof prf4
        rename_property_preserves_validity k k' (SObject sm) _ (Object vm) _ prf prf1 prf2 | (Just ksm, Nothing) | Just kvm =
            rewrite sym $ justInjective prf in
            rewrite sym prf1 in
            let
                split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                exist' = half_keys_eq_remove sm vm k (fst split)
                exist = half_keys_eq_insert (remove k sm) (remove k vm) k' ksm kvm exist'
                valid'' = still_valid vm sm k kvm ksm prf4 (cong fst prf3) (snd split)
                valid' = validate_properties_after_remove vm sm k (snd split)
                valid = validate_properties_after_insert (remove k vm) (remove k sm) k' kvm ksm valid'' valid'
            in rewrite exist in rewrite valid in Refl
        rename_property_preserves_validity k k' (SObject sm) _ (Object vm) _ prf prf1 prf2 | (Just kv, Nothing) | Nothing =
            let
                split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                contra' = not_half_keys_eq sm vm k (get_just_contains (cong fst prf3)) (get_nothing_contains prf4)
                contra = trans (sym contra') (fst split)
            in absurd contra

hoist_property_preserves_validity : (h, t : Key) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (HoistProperty h t) s = Just s' -> transform_value (HoistProperty h t) v = v' ->
    validate s v = True -> validate s' v' = True
hoist_property_preserves_validity _ _ SNull _ _ _ Refl _ _ impossible
hoist_property_preserves_validity _ _ SBoolean _ _ _ Refl _ _ impossible
hoist_property_preserves_validity _ _ SNumber _ _ _ Refl _ _ impossible
hoist_property_preserves_validity _ _ SText _ _ _ Refl _ _ impossible
hoist_property_preserves_validity _ _ (SArray _ _) _ _ _ Refl _ _ impossible
hoist_property_preserves_validity h t (SObject sm) s' v v' prf prf1 prf2 with (get h sm, get t sm) proof prf3
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Nothing, _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just SNull, _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just SBoolean, _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just SNumber, _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just SText, _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just (SArray _ _), _) = absurd $ prf
    hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just (SObject _), (Just _)) = absurd $ prf
    hoist_property_preserves_validity h t (SObject sm) s' v v' prf prf1 prf2 | (Just (SObject hsm), Nothing) with (get t hsm) proof prf4
        hoist_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just (SObject _), Nothing) | Nothing = absurd $ prf
        hoist_property_preserves_validity _ _ (SObject _) _ Null _ _ _ prf2 | (Just (SObject _), Nothing) | Just _ = absurd prf2
        hoist_property_preserves_validity _ _ (SObject _) _ (Primitive _) _ _ _ prf2 | (Just (SObject _), Nothing) | Just _ = absurd prf2
        hoist_property_preserves_validity _ _ (SObject _) _ (Array _) _ _ _ prf2 | (Just (SObject _), Nothing) | Just _ = absurd prf2
        hoist_property_preserves_validity h t (SObject sm) s' (Object vm) v' prf prf1 prf2 | (Just (SObject hsm), Nothing) | Just ts with (get h vm) proof prf5
            hoist_property_preserves_validity h _ (SObject sm) _ (Object vm) _ _ _prf2 | (Just (SObject _), Nothing) | Just _ | Nothing =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = not_half_keys_eq sm vm h (get_just_contains (cong fst prf3)) (get_nothing_contains prf5)
                    contra = trans (sym contra') (fst split)
                in absurd contra
            hoist_property_preserves_validity h _ (SObject sm) _ (Object vm) _ _ _ prf2 | (Just (SObject hsm), Nothing) | Just _ | Just Null =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h Null (SObject hsm) prf5 (cong fst prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            hoist_property_preserves_validity h _ (SObject sm) _ (Object vm) _ _ _ prf2 | (Just (SObject hsm), Nothing) | Just _ | Just (Primitive hvm) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h (Primitive hvm) (SObject hsm) prf5 (cong fst prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            hoist_property_preserves_validity h _ (SObject sm) _ (Object vm) _ _ _ prf2 | (Just (SObject hsm), Nothing) | Just _ | Just (Array hvm) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h (Array hvm) (SObject hsm) prf5 (cong fst prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            hoist_property_preserves_validity h t (SObject sm) s' (Object vm) v' prf prf1 prf2 | (Just (SObject hsm), Nothing) | Just ts | Just (Object hvm) with (get t hvm) proof prf6
                hoist_property_preserves_validity h t (SObject sm) s' (Object vm) v' prf prf1 prf2 | (Just (SObject hsm), Nothing) | Just ts | Just (Object hvm) | Nothing =
                    let
                        split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                        contra'' = not_half_keys_eq hsm hvm t (get_just_contains prf4) (get_nothing_contains prf6)
                        contra' = still_invalid vm sm h prf5 (cong fst prf3) (and_join2 contra'')
                        contra = trans (sym contra') (snd split)
                    in absurd contra
                hoist_property_preserves_validity h t (SObject sm) s' (Object vm) v' prf prf1 prf2 | (Just (SObject hsm), Nothing) | Just ts | Just (Object hvm) | (Just tv) =
                    rewrite sym $ justInjective prf in
                    rewrite sym prf1 in
                    let
                        split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                        exist' = half_keys_eq_insert sm vm t ts tv (fst split)
                        exist = half_keys_eq_insert (insert t ts sm) (insert t tv vm) h (SObject (remove t hsm)) (Object (remove t hvm)) exist'
                        valid''' = still_valid vm sm h (Object hvm) (SObject hsm) prf5 (cong fst prf3) (snd split)
                        split2 = and_split (half_keys_eq hsm hvm) (validate_properties hvm hsm) valid'''
                        valid'' = still_valid hvm hsm t tv ts prf6 prf4 (snd split2)
                        valid' = validate_properties_after_insert vm sm t tv ts valid'' (snd split)
                        exist2 = half_keys_eq_remove hsm hvm t (fst split2)
                        valid2 = validate_properties_after_remove hvm hsm t (snd split2)
                        join = and_join (exist2, valid2)
                        valid = validate_properties_after_insert (insert t tv vm) (insert t ts sm) h (Object (remove t hvm)) (SObject (remove t hsm)) join valid'
                    in rewrite exist in rewrite valid in Refl

plunge_property_preserves_validity : (h, t : Key) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (PlungeProperty h t) s = Just s' -> transform_value (PlungeProperty h t) v = v' ->
    validate s v = True -> validate s' v' = True
plunge_property_preserves_validity _ _ SNull _ _ _ Refl _ _ impossible
plunge_property_preserves_validity _ _ SBoolean _ _ _ Refl _ _ impossible
plunge_property_preserves_validity _ _ SNumber _ _ _ Refl _ _ impossible
plunge_property_preserves_validity _ _ SText _ _ _ Refl _ _ impossible
plunge_property_preserves_validity _ _ (SArray _ _) _ _ _ Refl _ _ impossible
plunge_property_preserves_validity h t (SObject sm) s' v v' prf prf1 prf2 with (get t sm, get h sm, t == h) proof prf3
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Nothing, _, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Nothing, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just SNull, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just SBoolean, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just SNumber, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just SText, _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just (SArray _ _), _) = absurd $ prf
    plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just (SObject _), True) = absurd $ prf
    plunge_property_preserves_validity h t (SObject sm) s' v v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) with (get t hsm) proof prf4
        plunge_property_preserves_validity _ _ (SObject _) _ _ _ prf _ _ | (Just _, Just (SObject _), False) | Just _ = absurd $ prf
        plunge_property_preserves_validity _ _ (SObject _) _ Null _ _ _ prf2 | (Just _, Just (SObject _), False) | Nothing = absurd prf2
        plunge_property_preserves_validity _ _ (SObject _) _ (Primitive _) _ _ _ prf2 | (Just _, Just (SObject _), False) | Nothing = absurd prf2
        plunge_property_preserves_validity _ _ (SObject _) _ (Array _) _ _ _ prf2 | (Just _, Just (SObject _), False) | Nothing = absurd prf2
        plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing with (get h vm, get t vm) proof prf5
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Nothing, _) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = not_half_keys_eq sm vm h (get_just_contains (cong (fst . snd) prf3)) (get_nothing_contains (cong fst prf5))
                    contra = trans (sym contra') (fst split)
                in absurd contra
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Just Null, _) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h Null (SObject hsm) (cong fst prf5) (cong (fst . snd) prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Just (Primitive hvm), _) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h (Primitive hvm) (SObject hsm) (cong fst prf5) (cong (fst . snd) prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Just (Array hvm), _) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = invalid_property vm sm h (Array hvm) (SObject hsm) (cong fst prf5) (cong (fst . snd) prf3) Refl
                    contra = trans (sym contra') (snd split)
                in absurd contra
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Just (Object hvm), Nothing) =
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    contra' = not_half_keys_eq sm vm t (get_just_contains (cong fst prf3)) (get_nothing_contains (cong snd prf5))
                    contra = trans (sym contra') (fst split)
                in absurd contra
            plunge_property_preserves_validity h t (SObject sm) v (Object vm) v' prf prf1 prf2 | (Just ts, Just (SObject hsm), False) | Nothing | (Just (Object hvm), Just tv) =
                rewrite sym $ justInjective prf in
                rewrite sym prf1 in
                let
                    split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    exist' = half_keys_eq_remove sm vm t (fst split)
                    exist = half_keys_eq_insert (remove t sm) (remove t vm) h (SObject (insert t ts hsm)) (Object (insert t tv hvm)) exist'
                    valid''' = still_valid vm sm h (Object hvm) (SObject hsm) (cong fst prf5) (cong (fst . snd) prf3) (snd split)
                    split2 = and_split (half_keys_eq hsm hvm) (validate_properties hvm hsm) valid'''
                    valid'' = still_valid vm sm t tv ts (cong snd prf5) (cong fst prf3) (snd split)
                    exist2 = half_keys_eq_insert hsm hvm t ts tv (fst split2)
                    valid2 = validate_properties_after_insert hvm hsm t tv ts valid'' (snd split2)
                    join = and_join (exist2, valid2)
                    valid' = validate_properties_after_remove vm sm t (snd split)
                    valid = validate_properties_after_insert (remove t vm) (remove t sm) h (Object (insert t tv hvm)) (SObject (insert t ts hsm)) join valid'
                in rewrite exist in rewrite valid in Refl

wrap_preserves_validity :
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema Wrap s = Just s' -> transform_value Wrap v = v' ->
    validate s v = True -> validate s' v' = True
wrap_preserves_validity _ _ _ _ prf prf1 prf2 =
    rewrite sym $ justInjective prf in rewrite sym prf1 in rewrite prf2 in Refl

head_preserves_validity :
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema Head s = Just s' -> transform_value Head v = v' ->
    validate s v = True -> validate s' v' = True
head_preserves_validity SNull _ _ _ Refl _ _ impossible
head_preserves_validity SBoolean _ _ _ Refl _ _ impossible
head_preserves_validity SNumber _ _ _ Refl _ _ impossible
head_preserves_validity SText _ _ _ Refl _ _ impossible
head_preserves_validity (SArray False _) _ Null _ _ _ Refl impossible
head_preserves_validity (SArray False _) _ (Primitive _) _ _ _ Refl impossible
head_preserves_validity (SArray False _) _ (Array []) _ _ _ Refl impossible
head_preserves_validity (SArray False s) _ (Array (h :: xs)) _ prf prf1 prf2 =
    rewrite sym $ justInjective prf in rewrite sym prf1 in
    let split = and_split (validate s h) (validate (SArray True s) (Array xs)) prf2 in
    rewrite fst split in Refl
head_preserves_validity (SArray False _) _ (Object _) _ _ _ Refl impossible
head_preserves_validity (SArray True _) _ _ _ Refl _ _ impossible
head_preserves_validity (SObject _) _ _ _ Refl _ _ impossible

convert_preserves_validity : (k, k' : PrimitiveKind) -> (m : List (PrimitiveValue, PrimitiveValue)) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema (Convert k k' m) s = Just s' -> transform_value (Convert k k' m) v = v' ->
    validate s v = True -> validate s' v' = True
convert_preserves_validity k k' m s s' v v' prf prf1 prf2 with (validate_map k k' m) proof prf3
    convert_preserves_validity KBoolean KBoolean _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KBoolean KText _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KNumber KNumber _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KNumber KText _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KText KBoolean _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KText KNumber _ _ _ _ _ prf _ _ | False = absurd $ prf
    convert_preserves_validity KText KText _ _ _ _ _ prf _ _ | False = absurd $ prf

    convert_preserves_validity KBoolean KBoolean _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KText _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KBoolean _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KText _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KBoolean _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KText _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KBoolean _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KText _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KBoolean _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KNumber _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KBoolean KText _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KNumber _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KText _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KNumber _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KText _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KNumber _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KText _ SText _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KNumber _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KText _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KBoolean _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KNumber _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KNumber KText _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KBoolean _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KNumber _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KText _ SNull _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KBoolean _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KNumber _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KText _ SBoolean _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KBoolean _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KNumber _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KText _ SNumber _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KBoolean _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KNumber _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KText _ (SArray _ _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KBoolean _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KNumber _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf
    convert_preserves_validity KText KText _ (SObject _) _ _ _ prf _ _ | True = absurd $ prf

    convert_preserves_validity KBoolean KBoolean _ SBoolean SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KNumber _ SBoolean SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KText _ SBoolean SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KNumber _ SBoolean SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KText _ SBoolean SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KBoolean _ SBoolean SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KText _ SBoolean SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KBoolean _ SBoolean SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KNumber _ SBoolean SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KBoolean _ SBoolean (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KNumber _ SBoolean (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KText _ SBoolean (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KBoolean _ SBoolean (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KNumber _ SBoolean (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KBoolean KText _ SBoolean (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KBoolean _ SNumber SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KNumber _ SNumber SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KText _ SNumber SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KNumber _ SNumber SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KText _ SNumber SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KBoolean _ SNumber SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KText _ SNumber SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KBoolean _ SNumber SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KNumber _ SNumber SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KBoolean _ SNumber (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KNumber _ SNumber (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KText _ SNumber (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KBoolean _ SNumber (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KNumber _ SNumber (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KNumber KText _ SNumber (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KBoolean _ SText SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KNumber _ SText SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KText _ SText SNull _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KNumber _ SText SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KText _ SText SBoolean _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KBoolean _ SText SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KText _ SText SNumber _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KBoolean _ SText SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KNumber _ SText SText _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KBoolean _ SText (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KNumber _ SText (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KText _ SText (SArray _ _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KBoolean _ SText (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KNumber _ SText (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf
    convert_preserves_validity KText KText _ SText (SObject _) _ _ prf _ _ | True = absurd $ justInjective prf

    convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KNumber _ SBoolean SNumber Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KText _ SBoolean SText Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KText _ SBoolean SText (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KText _ SBoolean SText (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KText _ SBoolean SText (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KBoolean KText _ SBoolean SText (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KBoolean _ SNumber SBoolean Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KNumber _ SNumber SNumber Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KNumber _ SNumber SNumber (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KNumber _ SNumber SNumber (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KNumber _ SNumber SNumber (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KNumber _ SNumber SNumber (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KText _ SNumber SText Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KText _ SNumber SText (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KText _ SNumber SText (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KText _ SNumber SText (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KNumber KText _ SNumber SText (Primitive (Text _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KBoolean _ SText SBoolean Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KBoolean _ SText SBoolean (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KBoolean _ SText SBoolean (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KBoolean _ SText SBoolean (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KBoolean _ SText SBoolean (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KNumber _ SText SNumber Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KNumber _ SText SNumber (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KNumber _ SText SNumber (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KNumber _ SText SNumber (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KNumber _ SText SNumber (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KText _ SText SText Null _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KText _ SText SText (Array _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KText _ SText SText (Object _) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KText _ SText SText (Primitive (Boolean _)) _ _ _ prf2 | True = absurd prf2
    convert_preserves_validity KText KText _ SText SText (Primitive (Number _)) _ _ _ prf2 | True = absurd prf2

    convert_preserves_validity KBoolean KBoolean m SBoolean SBoolean (Primitive (Boolean va)) v' prf prf1 prf2 | True with (convert_prim (Boolean va) m) proof prf4
        convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Primitive (Boolean _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KBoolean _ SBoolean SBoolean (Primitive (Boolean _)) _ _ prf1 _ | True | (Just (Boolean _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KBoolean m SBoolean SBoolean (Primitive (Boolean va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KBoolean KBoolean (Boolean va) (Number vb) prf3 Refl prf4
        convert_preserves_validity KBoolean KBoolean m SBoolean SBoolean (Primitive (Boolean va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KBoolean KBoolean (Boolean va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KBoolean KNumber m SBoolean SNumber (Primitive (Boolean va)) v' prf prf1 prf2 | True with (convert_prim (Boolean va) m) proof prf4
        convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Primitive (Boolean _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KNumber _ SBoolean SNumber (Primitive (Boolean _)) _ _ prf1 _ | True | (Just (Number _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KNumber m SBoolean SNumber (Primitive (Boolean va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KBoolean KNumber (Boolean va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KBoolean KNumber m SBoolean SNumber (Primitive (Boolean va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KBoolean KNumber (Boolean va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KBoolean KText m SBoolean SText (Primitive (Boolean va)) v' prf prf1 prf2 | True with (convert_prim (Boolean va) m) proof prf4
        convert_preserves_validity KBoolean KText _ SBoolean SText (Primitive (Boolean _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KText _ SBoolean SText (Primitive (Boolean _)) _ _ prf1 _ | True | (Just (Text _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KBoolean KText m SBoolean SText (Primitive (Boolean va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KBoolean KText (Boolean va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KBoolean KText m SBoolean SText (Primitive (Boolean va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KBoolean KText (Boolean va) (Number vb) prf3 Refl prf4
    convert_preserves_validity KNumber KBoolean m SNumber SBoolean (Primitive (Number va)) v' prf prf1 prf2 | True with (convert_prim (Number va) m) proof prf4
        convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Primitive (Number _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KBoolean _ SNumber SBoolean (Primitive (Number _)) _ _ prf1 _ | True | (Just (Boolean _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KBoolean m SNumber SBoolean (Primitive (Number va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KNumber KBoolean (Number va) (Number vb) prf3 Refl prf4
        convert_preserves_validity KNumber KBoolean m SNumber SBoolean (Primitive (Number va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KNumber KBoolean (Number va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KNumber KNumber m SNumber SNumber (Primitive (Number va)) v' prf prf1 prf2 | True with (convert_prim (Number va) m) proof prf4
        convert_preserves_validity KNumber KNumber _ SNumber SNumber (Primitive (Number _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KNumber _ SNumber SNumber (Primitive (Number _)) _ _ prf1 _ | True | (Just (Number _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KNumber m SNumber SNumber (Primitive (Number va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KNumber KNumber (Number va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KNumber KNumber m SNumber SNumber (Primitive (Number va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KNumber KNumber (Number va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KNumber KText m SNumber SText (Primitive (Number va)) v' prf prf1 prf2 | True with (convert_prim (Number va) m) proof prf4
        convert_preserves_validity KNumber KText _ SNumber SText (Primitive (Number _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KText _ SNumber SText (Primitive (Number _)) _ _ prf1 _ | True | (Just (Text _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KNumber KText m SNumber SText (Primitive (Number va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KNumber KText (Number va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KNumber KText m SNumber SText (Primitive (Number va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KNumber KText (Number va) (Number vb) prf3 Refl prf4
    convert_preserves_validity KText KBoolean m SText SBoolean (Primitive (Text va)) v' prf prf1 prf2 | True with (convert_prim (Text va) m) proof prf4
        convert_preserves_validity KText KBoolean _ SText SBoolean (Primitive (Text _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KBoolean _ SText SBoolean (Primitive (Text _)) _ _ prf1 _ | True | (Just (Boolean _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KBoolean m SText SBoolean (Primitive (Text va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KText KBoolean (Text va) (Number vb) prf3 Refl prf4
        convert_preserves_validity KText KBoolean m SText SBoolean (Primitive (Text va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KText KBoolean (Text va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KText KNumber m SText SNumber (Primitive (Text va)) v' prf prf1 prf2 | True with (convert_prim (Text va) m) proof prf4
        convert_preserves_validity KText KNumber _ SText SNumber (Primitive (Text _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KNumber _ SText SNumber (Primitive (Text _)) _ _ prf1 _ | True | (Just (Number _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KNumber m SText SNumber (Primitive (Text va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KText KNumber (Text va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KText KNumber m SText SNumber (Primitive (Text va)) _ _ _ _ | True | (Just (Text vb)) =
            absurd $ convert_prim_kind m KText KNumber (Text va) (Text vb) prf3 Refl prf4
    convert_preserves_validity KText KText m SText SText (Primitive (Text va)) v' prf prf1 prf2 | True with (convert_prim (Text va) m) proof prf4
        convert_preserves_validity KText KText _ SText SText (Primitive (Text _)) _ _ prf1 _ | True | Nothing =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KText _ SText SText (Primitive (Text _)) _ _ prf1 _ | True | (Just (Text _)) =
            rewrite sym prf1 in Refl
        convert_preserves_validity KText KText m SText SText (Primitive (Text va)) _ _ _ _ | True | (Just (Boolean vb)) =
            absurd $ convert_prim_kind m KText KText (Text va) (Boolean vb) prf3 Refl prf4
        convert_preserves_validity KText KText m SText SText (Primitive (Text va)) _ _ _ _ | True | (Just (Number vb)) =
            absurd $ convert_prim_kind m KText KText (Text va) (Number vb) prf3 Refl prf4

||| Transforming a valid value must result in a valid value
lens_preserves_validity : (l : Lens) ->
    (s : Schema) -> (s' : Schema) -> (v : Value) -> (v' : Value) ->
    transform_schema l s = Just s' -> transform_value l v = v' ->
    validate s v = True -> validate s' v' = True
lens_preserves_validity (Make k) s s' v v' prf prf1 prf2 =
    make_preserves_validity k s s' v v' prf prf1 prf2
lens_preserves_validity (Destroy k) s s' v v' prf prf1 prf2 =
    destroy_preserves_validity k s s' v v' prf prf1 prf2
lens_preserves_validity (AddProperty k) s s' v v' prf prf1 prf2 =
    add_property_preserves_validity k s s' v v' prf prf1 prf2
lens_preserves_validity (RemoveProperty k) s s' v v' prf prf1 prf2 =
    remove_property_preserves_validity k s s' v v' prf prf1 prf2
lens_preserves_validity (RenameProperty k k') s s' v v' prf prf1 prf2 =
    rename_property_preserves_validity k k' s s' v v' prf prf1 prf2
lens_preserves_validity (HoistProperty h t) s s' v v' prf prf1 prf2 =
    hoist_property_preserves_validity h t s s' v v' prf prf1 prf2
lens_preserves_validity (PlungeProperty h t) s s' v v' prf prf1 prf2 =
    plunge_property_preserves_validity h t s s' v v' prf prf1 prf2
lens_preserves_validity Wrap s s' v v' prf prf1 prf2 =
    wrap_preserves_validity s s' v v' prf prf1 prf2
lens_preserves_validity Head s s' v v' prf prf1 prf2 =
    head_preserves_validity s s' v v' prf prf1 prf2
lens_preserves_validity (LensIn _ _) SNull _ _ _ Refl _ _ impossible
lens_preserves_validity (LensIn _ _) SBoolean _ _ _ Refl _ _ impossible
lens_preserves_validity (LensIn _ _) SNumber _ _ _ Refl _ _ impossible
lens_preserves_validity (LensIn _ _) SText _ _ _ Refl _ _ impossible
lens_preserves_validity (LensIn _ _) (SArray _ _) _ _ _ Refl _ _ impossible
lens_preserves_validity (LensIn _ _) (SObject _) _ Null _ _ _ Refl impossible
lens_preserves_validity (LensIn _ _) (SObject _) _ (Primitive _) _ _ _ Refl impossible
lens_preserves_validity (LensIn _ _) (SObject _) _ (Array _) _ _ _ Refl impossible
lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 with (get k sm) proof prf3
    lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Nothing = absurd $ prf
    lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Just s2 with (get k vm) proof prf4
        lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Just s2 | Nothing =
            let split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                invalid = not_half_keys_eq sm vm k (get_just_contains prf3) (get_nothing_contains prf4)
                contra = trans (sym invalid) (fst split)
            in absurd contra
        lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Just s2 | Just v2 with (transform_schema l s2) proof prf5
            lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Just s2 | Just v2 | Nothing = absurd $ prf
            lens_preserves_validity (LensIn k l) (SObject sm) s' (Object vm) v' prf prf1 prf2 | Just s2 | Just v2 | Just s2' =
                rewrite sym $ justInjective prf in
                rewrite sym $ prf1 in
                let split = and_split (half_keys_eq sm vm) (validate_properties vm sm) prf2
                    still = still_valid vm sm k v2 s2 prf4 prf3 (snd split)
                    ind = lens_preserves_validity l s2 s2' v2 (transform_value l v2) prf5 Refl still
                    exist = half_keys_eq_insert sm vm k s2' (transform_value l v2) (fst split)
                    valid = validate_properties_after_insert vm sm k (transform_value l v2) s2' ind (snd split)
                in rewrite exist in valid
lens_preserves_validity (LensMap _) SNull _ _ _ Refl _ _ impossible
lens_preserves_validity (LensMap _) SBoolean _ _ _ Refl _ _ impossible
lens_preserves_validity (LensMap _) SNumber _ _ _ Refl _ _ impossible
lens_preserves_validity (LensMap _) SText _ _ _ Refl _ _ impossible
lens_preserves_validity (LensMap _) (SArray _ _) _ Null _ _ _ Refl impossible
lens_preserves_validity (LensMap _) (SArray _ _) _ (Primitive _) _ _ _ Refl impossible
lens_preserves_validity (LensMap l) (SArray e s2) s' (Array xs) v' prf prf1 prf2 with (transform_schema l s2) proof prf3
    lens_preserves_validity (LensMap _) (SArray _ _) SNull (Array _) _ prf _ _ | (Just _) =
        absurd $ justInjective $ prf
    lens_preserves_validity (LensMap _) (SArray _ _) SBoolean (Array _) _ prf _ _ | (Just _) =
        absurd $ justInjective $ prf
    lens_preserves_validity (LensMap _) (SArray _ _) SNumber (Array _) _ prf _ _ | (Just _) =
        absurd $ justInjective $ prf
    lens_preserves_validity (LensMap _) (SArray _ _) SText (Array _) _ prf _ _ | (Just _) =
        absurd $ justInjective $ prf
    lens_preserves_validity (LensMap _) (SArray _ _) (SObject _) (Array _) _ prf _ _ | (Just _) =
        absurd $ justInjective $ prf
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array _) Null _ prf1 _ | (Just _) =
        absurd $ prf1
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array _) (Primitive _) _ prf1 _ | (Just _) =
        absurd $ prf1
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array _) (Object _) _ prf1 _ | (Just _) =
        absurd $ prf1
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array []) (Array (_ :: _)) _ prf1 _ | (Just _) =
        absurd $ prf1
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array (_ :: _)) (Array []) _ prf1 _ | (Just _) =
        absurd $ prf1
    lens_preserves_validity (LensMap _) (SArray _ _) (SArray _ _) (Array []) (Array []) prf _ prf2 | (Just _) =
        rewrite sym $ justInjective $ cong allow_empty $ justInjective prf in
        rewrite prf2 in Refl
    lens_preserves_validity (LensMap l) (SArray e s2) (SArray e' s2') (Array (v2 :: xs)) (Array (v2' :: xs')) prf prf1 prf2 | (Just s2'2) with (validate s2 v2) proof prf4
        lens_preserves_validity (LensMap l) (SArray e s2) (SArray e' s2') (Array (v2 :: xs)) (Array (v2' :: xs')) prf prf1 prf2 | (Just s2'2) | False = absurd $ prf2
        lens_preserves_validity (LensMap l) (SArray e s2) (SArray e' s2') (Array (v2 :: xs)) (Array (v2' :: xs')) prf prf1 prf2 | (Just s2'2) | True =
            let eqs = trans prf3 $ cong sarray $ justInjective prf
                eqv = consInjective $ justInjective $ cong array prf1
                ind = lens_preserves_validity l s2 s2' v2 v2' eqs (fst eqv) prf4
            in rewrite ind in
            let ind = lens_preserves_validity (LensMap l) (SArray True s2) (SArray True s2') (Array xs) (Array xs')
            in ?hhhhhhh

lens_preserves_validity (LensMap _) (SArray _ _) _ (Object _) _ _ _ Refl impossible
lens_preserves_validity (LensMap _) (SObject _) _ _ _ Refl _ _ impossible
lens_preserves_validity (Convert k k' m) s s' v v' prf prf1 prf2 =
    convert_preserves_validity k k' m s s' v v' prf prf1 prf2

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria


text:
module decDivZ
import ZZ
import ZZUtils
import Divisors
import GCDZZ
import Primes
import gcd
%access public export
%default total

isDivisibleImpliesIsDivisibleZ:isDivisible a b ->
          IsDivisibleZ (Pos a) (Pos b)
isDivisibleImpliesIsDivisibleZ (n**(gpf,eqpf)) = ((Pos n)**(cong eqpf))

posIntToSuccNat:{m:ZZ}->(IsPositive m) ->(t:Nat**(((m = (Pos t)),(IsSucc t))))
posIntToSuccNat {m = (Pos (S k))} Positive = ((S k)**(Refl,(ItIsSucc )))

succGtZero:{t:Nat}->(IsSucc t)->GT t Z
succGtZero {t = (S n)} ItIsSucc = LTESucc LTEZero

rehelp2:{m:ZZ}->{k:ZZ}->(s:ZZ)-> m = k->s*k = s*m
rehelp2  s prf = rewrite sym $ prf in
              Refl

isDivisibleZImpliesIsDivisible :{a:Nat}->{b:Nat}->
     IsPositive (Pos a) -> IsDivisibleZ (Pos a) (Pos b) ->isDivisible a b
isDivisibleZImpliesIsDivisible {a = (S k)}{b = Z}  Positive x =
    void (zeroDoesntDivideNonZero PositiveZ x)
isDivisibleZImpliesIsDivisible {a = (S k)}{b = (S j)} Positive (m**eqpf) =
  (case posDivByPosIsPos {c = (Pos (S k))}{d =(Pos (S j))} Positive Positive  eqpf of
        mPos => (case posIntToSuccNat mPos of
                  (t**(equal,tsucc)) => ( t**((succGtZero tsucc),( posInjective( rewrite rehelp2 {m=m}{k=(Pos t)} (Pos (S j)) equal   in
                                                                  eqpf))))))

posSSknotOne: (Pos ( S (S k)))=1->Void
posSSknotOne Refl impossible

posSSknotMinusOne: (Pos ( S (S k)))=(-1)->Void
posSSknotMinusOne Refl impossible

gt2DoesntDivideOne: {k:Nat}->IsDivisibleZ 1 (Pos ( S (S k)))  ->Void
gt2DoesntDivideOne {k} (n**eqpf) =
  (case productOneThenNumbersOne (Pos (S (S k))) n (sym eqpf) of
        (Left (a, b)) => posSSknotOne a
        (Right (a, b)) => posSSknotMinusOne a)

succNotZ:( S n) = Z ->Void
succNotZ Refl impossible

decDivisibleZnn: (a:ZZ)->(b:ZZ)->IsNonNegative a->IsNonNegative b -> Dec (IsDivisibleZ a b)
decDivisibleZnn (Pos Z) b NonNegative y = Yes (zzDividesZero _)
decDivisibleZnn (Pos (S Z)) (Pos Z) NonNegative NonNegative = No (zeroDoesntDivideNonZero PositiveZ )
decDivisibleZnn (Pos (S Z)) (Pos (S Z)) NonNegative NonNegative= Yes ( oneDiv 1)
decDivisibleZnn (Pos (S Z)) (Pos (S (S k))) NonNegative NonNegative= No (gt2DoesntDivideOne )
decDivisibleZnn (Pos (S (S k))) (Pos Z) NonNegative NonNegative= No (zeroDoesntDivideNonZero PositiveZ )
decDivisibleZnn (Pos (S (S k))) (Pos (S j)) NonNegative NonNegative=
   (case decDiv (S (S k)) (LTESucc (LTESucc LTEZero)) (S j)
               {euc = eculidDivideAux (S(S k)) (S j) (succNotZ)} of
         (Yes prf) => (Yes (isDivisibleImpliesIsDivisibleZ prf))
         (No contra) => No(contra . (isDivisibleZImpliesIsDivisible {b =(S j)} Positive)))

|||Given two integers , a and b, it either returns a proof that  b|a or
||| a proof that b|a is impossible.
decDivisibleZ: (a:ZZ)->(b:ZZ)->(Dec (IsDivisibleZ a b))
decDivisibleZ (Pos k) (Pos j) =
  decDivisibleZnn (Pos k) (Pos j) NonNegative NonNegative
decDivisibleZ (Pos k) (NegS j) =
  (case decDivisibleZnn (Pos k) (-(NegS j)) NonNegative NonNegative of
        (Yes prf) => Yes (negativeDivides prf )
        (No contra) => No (contra . negativeDivides {d =NegS j} ))
decDivisibleZ (NegS k) (Pos j) =
  (case decDivisibleZnn (-(NegS k)) (Pos j) NonNegative NonNegative of
        (Yes prf) => Yes ( dDividesNegative prf)
        (No contra) => No (contra . dDividesNegative {a = (NegS k)}))
decDivisibleZ (NegS k) (NegS j) =
  (case decDivisibleZnn (-(NegS k)) (-(NegS j)) NonNegative NonNegative of
        (Yes prf) => Yes ( dDividesNegative (negativeDivides prf))
        (No contra) => No ( contra . doubleNegativeDivides { a =NegS k}{d = NegS j}))

ext: idr


text:
module Highlight.Parser

import Highlight.Regions

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Char
import Lightyear.Strings

||| The data format output by Idris's highlighting routines
public export
data SExpr = SSym String | SString String | SInt Integer | SList (List SExpr)

%name SExpr sexp

export
Show SExpr where
  show (SSym x) = ":" ++ x
  show (SString x) = show x
  show (SInt x) = show x
  show (SList xs) = "(" ++ concat (intersperse " " (map show xs)) ++ ")"

sSymInj : SSym x = SSym y -> x = y
sSymInj Refl = Refl

sStringInj : SString x = SString y -> x = y
sStringInj Refl = Refl

sIntInj : SInt x = SInt y -> x = y
sIntInj Refl = Refl

sListInj : SList xs = SList ys -> xs = ys
sListInj Refl = Refl

DecEq SExpr where
  decEq (SSym x) (SSym y) with (decEq x y)
    decEq (SSym x) (SSym x) | Yes Refl  = Yes Refl
    decEq (SSym x) (SSym y) | No contra = No $ contra . sSymInj
  decEq (SSym x) (SString y) = No $ \(Refl) impossible
  decEq (SSym x) (SInt y) = No $ \(Refl) impossible
  decEq (SSym x) (SList xs) = No $ \(Refl) impossible
  decEq (SString x) (SSym y) = No $ \(Refl) impossible
  decEq (SString x) (SString y) with (decEq x y)
    decEq (SString x) (SString x) | Yes Refl  = Yes Refl
    decEq (SString x) (SString y) | No contra = No $ contra . sStringInj
  decEq (SString x) (SInt y) = No $ \(Refl) impossible
  decEq (SString x) (SList xs) = No $ \(Refl) impossible
  decEq (SInt x) (SSym y) = No $ \(Refl) impossible
  decEq (SInt x) (SString y) = No $ \(Refl) impossible
  decEq (SInt x) (SInt y) with (decEq x y)
    decEq (SInt x) (SInt x) | Yes Refl  = Yes Refl
    decEq (SInt x) (SInt y) | No contra = No $ contra . sIntInj
  decEq (SInt x) (SList xs) = No $ \(Refl) impossible
  decEq (SList xs) (SSym x) = No $ \(Refl) impossible
  decEq (SList xs) (SString x) = No $ \(Refl) impossible
  decEq (SList xs) (SInt x) = No $ \(Refl) impossible
  decEq (SList xs) (SList ys) with (assert_total $ decEq xs ys)
    decEq (SList xs) (SList xs) | Yes Refl  = Yes Refl
    decEq (SList xs) (SList ys) | No contra = No $ contra . sListInj

namespace Assoc
  ||| Because much of the highlighting information is in alist form,
  ||| we need a representation that lets us do lookups in alists. This
  ||| datatype represents the results of those lookups.
  |||
  ||| This datatype is slightly deficient - it should guarantee that
  ||| we find the _first_ matching key, but it only guarantees that we
  ||| find _a_ matching key. Ah well, duplicate keys don't occur in
  ||| Idris's highlighting output.
  |||
  ||| @ needle what we are looking for
  ||| @ value the associated information, once found
  ||| @ haystack where we are looking
  data Assoc : (needle : SExpr) -> (value : List SExpr) -> (haystack : List SExpr) -> Type where
    ||| The key was found at the beginning
    Car : Assoc k v (SList (k :: v) :: sexprs)
    ||| The key was found in the tail
    Cdr : Assoc k v sexprs -> Assoc k v (sexpr :: sexprs)

  total
  noAssocEmpty : Assoc needle value [] -> Void
  noAssocEmpty Car impossible
  noAssocEmpty (Cdr prf) impossible

  total
  assocConsNotList : Assoc needle value (headSexpr :: sexprs) ->
                     Not (xs : List SExpr ** headSexpr = SList xs) ->
                     Assoc needle value sexprs
  assocConsNotList (Cdr x) notEqList = x
  assocConsNotList Car nope = absurd $ nope (_ ** Refl)

  total
  assocNonEmpty : Assoc needle value (SList [] :: sexprs) -> Assoc needle value sexprs
  assocNonEmpty (Cdr x) = x

  -- The following function could probably be cleaned up a bit, but that would require real thought...
  ||| Do a lookup in an alist.
  total
  assoc : (needle : SExpr) -> (haystack : List SExpr) -> Dec (value : List SExpr ** Assoc needle value haystack)
  assoc needle [] = No $ \(v ** prf) => noAssocEmpty prf
  assoc needle (SSym x :: xs) with (assoc needle xs)
    assoc needle (SSym x :: xs) | Yes prf   = Yes (fst prf ** Cdr (snd prf))
    assoc needle (SSym x :: xs) | No contra =
      No $ \(value ** location) =>
        contra (value ** assocConsNotList location (\(xs ** Refl) impossible))
  assoc needle (SString x :: xs) with (assoc needle xs)
    assoc needle (SString x :: xs) | Yes prf   = Yes (fst prf ** Cdr (snd prf))
    assoc needle (SString x :: xs) | No contra =
      No $ \(value ** location) =>
        contra (value ** assocConsNotList location (\(xs ** Refl) impossible))
  assoc needle (SInt x :: xs) with (assoc needle xs)
    assoc needle (SInt x :: xs) | Yes prf   = Yes (fst prf ** Cdr (snd prf))
    assoc needle (SInt x :: xs) | No contra =
      No $ \(value ** location) =>
        contra (value ** assocConsNotList location (\(xs ** Refl) impossible))
  assoc needle (SList [] :: xs) with (assoc needle xs)
    assoc needle (SList [] :: xs) | Yes prf   = Yes (fst prf ** Cdr (snd prf))
    assoc needle (SList [] :: xs) | No contra =
      No $ \(value ** location) =>
        contra (value ** assocNonEmpty location)
  assoc needle (SList (y :: ys) :: xs) with (decEq needle y)
    assoc needle (SList (needle :: ys) :: xs) | Yes Refl = Yes (_ ** Car)
    assoc needle (SList (y :: ys) :: xs) | No notHere with (assoc needle xs)
      assoc needle (SList (y :: ys) :: xs) | No notHere | Yes prf = Yes (fst prf ** Cdr (snd prf))
      assoc needle (SList (y :: ys) :: xs) | No notHere | No notThere =
        No $ \(value ** location) =>
          case location of
            Car => notHere Refl
            Cdr tl => notThere (_ ** tl)

||| Parse a parenthesized sequence
inParens : Parser a -> Parser a
inParens p = token "(" *!> p <* token ")"

||| Parse the end of an escape sequence in a string
escaped : Parser Char
escaped = char '\\' <|>| char '"' -- TODO - more?

||| Parse a single character from a string (possibly an escape sequence)
stringChar : Parser Char
stringChar = (char '\\' *!> escaped) <|>| (satisfy (\c => c /= '\\' && c /= '"'))

||| Parse a string literal
stringLit : Parser String
stringLit = lexeme $ char '"' *!> (pack <$> many stringChar) <* char '"'

||| Parse a character that is allowed as part of a symbol name
symbolChar : Parser Char
symbolChar = satisfy (\c => ('a' <= c && c <= 'z') ||
                            ('A' <= c && c <= 'Z') ||
                            ('0' <= c && c <= '9') ||
                            (c == '-'))

||| Parse a symbol
symbol : Parser String
symbol = lexeme $ char ':' *> (pack <$> many symbolChar)

||| Parse a whole S-expression
export
expr : Parser SExpr
expr =      SString <$> stringLit
       <|>| SSym <$> symbol
       <|>| SInt <$> lexeme integer
       <|>| SList <$> inParens (many expr)

decToMaybe : Dec a -> Maybe a
decToMaybe (Yes p) = Just p
decToMaybe (No _) = Nothing

total
getRegion : SExpr -> Maybe (Region ())
getRegion (SList xs) = do ([SString fn] ** _) <- decToMaybe (assoc (SSym "filename") xs)
                            | _ => Nothing
                          ([SInt sl, SInt sc] ** _) <- decToMaybe (assoc (SSym "start") xs)
                            | _ => Nothing
                          ([SInt el, SInt ec] ** _) <- decToMaybe (assoc (SSym "end") xs)
                            | _ => Nothing
                          pure (MkRegion fn sl sc el (1 + ec) ())
getRegion _ = Nothing

export
getRegionMeta : SExpr -> Maybe (Region SExpr)
getRegionMeta (SList [r, meta]) = map (const meta) <$> getRegion r
getRegionMeta _ = Nothing

getHighlightType : SExpr -> Maybe HighlightType
getHighlightType (SList xs) = do ([SSym d] ** _) <- decToMaybe (assoc (SSym "decor") xs)
                                   | _ => Nothing
                                 case d of
                                   "bound" => Just (Bound False) -- TODO look for implicit
                                   "keyword" => Just Keyword
                                   other =>
                                     [| Name (isName other) (pure $ getDocstring xs) (pure $ getType xs) |]
  where
    isName : String -> Maybe NameHL
    isName "function" = Just Function
    isName "data"     = Just Constructor
    isName "type"     = Just TypeConstructor
    isName _          = Nothing
    getDocstring : List SExpr -> String
    getDocstring xs = case decToMaybe $ assoc (SSym "doc-overview") xs of
                        Just ([SString d] ** _) => d
                        _ => ""
    getType : List SExpr -> String
    getType xs = case decToMaybe $ assoc (SSym "type") xs of
                        Just ([SString d] ** _) => d
                        _ => ""
getHighlightType _ = Nothing

export
mkHls : List (Region SExpr) -> List (Region HighlightType)
mkHls [] = []
mkHls (r::rs) = case getHighlightType (metadata r) of
                  Nothing => mkHls rs
                  Just hl => map (const hl) r :: mkHls rs


text:
module Main

import Data.Vect

record Foo (n : Nat) where
  constructor MkFoo
  name : String
  things : Vect n a
  more_things : Vect m b

record Person where
  constructor MkPerson
  name : String
  age : Int

testFoo : Foo 3
testFoo = MkFoo "name" [1,2,3] [4,5,6,7]

person : Person
person = MkPerson "Fred" 30

main : IO ()
main = do let x = record { name = "foo",
                           more_things = reverse ["a","b"] } testFoo
          printLn $ name x
          printLn $ name person
          printLn $ things x
          printLn $ more_things x
          printLn $ age (record { age = 25 } person)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
import Data.Vect

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

triangle : Polygon 3
triangle = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (b : Bool) -> StringOrInt b
getStringOrInt False = "Ninety four"
getStringOrInt True = 94

-- valToString : (isInt : Bool) -> StringOrInt isInt -> String
-- valToString False x = trim x
-- valToString True x = cast x

valToString : (isInt : Bool) -> (case isInt of
                                      False => String
                                      True => Int) -> String
valToString False y = trim y
valToString True y = cast y

-- Should be a profunctor
MultivariableFunction : Nat -> Type -> Type -> Type
MultivariableFunction Z argumentType resultType = resultType
MultivariableFunction (S k) argumentType resultType =
  argumentType -> MultivariableFunction k argumentType resultType

multiAdder : (n : Nat) -> Nat -> MultivariableFunction n Nat Nat
multiAdder Z n = n
multiAdder (S argsToReceiveCount) n =
  (\receivedNat => multiAdder argsToReceiveCount (n + receivedNat))

asMultiVariable : (a -> a -> a) -> (n : Nat) -> a -> MultivariableFunction n a a
asMultiVariable f Z x = x
asMultiVariable f (S k) x =
  (\receivedArg => asMultiVariable f k (f x receivedArg))

multiProduct : (n : Nat) -> Nat -> MultivariableFunction n Nat Nat
multiProduct = asMultiVariable (*)


text:
allLengths : List String -> List Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

mutual
    isEven : Nat -> Bool
    isEven Z = True
    isEven (S k) = isOdd k

    isOdd : Nat -> Bool
    isOdd Z = False
    isOdd (S k) = isEven k

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Util

-- NB things will need to be removed from here as Idris gains them in the
-- Prelude.

import System.File

infixl 1 <&>
export
(<&>) : Functor f => f a -> (a -> b) -> f b
x <&> f = f <$> x

infixr 1 =<<
export
(=<<) : Monad m => (a -> m b) -> m a -> m b
(=<<) = flip (>>=)

-- For when Lazy is causing type problems and you want to avoid Force/Delay, or
-- force/delay isn't working as I've noticed it sometimes doesn't.
infixr 4 &&|
export
(&&|) : Bool -> Bool -> Bool
(&&|) x y = x && y

export
catMaybes : List (Maybe a) -> List a
catMaybes z = foldr (\m,f => maybe f (\x => (x ::) . f) m) id z []

export
isJust : Maybe a -> Bool
isJust (Just _ ) = True
isJust _ = False

export
unzip : List (a,b) -> (List a, List b)
unzip = foldr (\(x,y),(xs,ys) => (x :: xs, y :: ys)) ([],[])

-- This is hiiiiiideously slow! maybe it's because I'm using it at elab-time
export
unzip3 : List (a,b,c) -> (List a, List b, List c)
unzip3 [] = ([],[],[])
unzip3 ((x, (y, z)) :: ls) = let (xs,ys,zs) = unzip3 ls
                             in (x :: xs, y:: ys, z :: zs)

export
unless : Applicative f => Bool -> Lazy (f ()) -> f ()
unless b act = if b then pure () else act

public export
monus : Nat -> Nat -> Nat
monus Z _ = Z
monus k Z = k
monus (S k) (S j) = k `monus`j

export
withFile : HasIO io => String -> Mode -> (Either FileError File -> io a) -> io a
withFile file mode act = do res <- openFile file mode
                            a <- act res
                            either (\_ => pure a)
                                   (\f => pure a <* closeFile f) res

export
on : (b -> b -> c) -> (a -> b) -> a -> a -> c
on f g x y = g x `f` g y

infixl 9 ^
export
%foreign "scheme:expt"
(^) : Int -> Int -> Int

infixl 7 .&.
export
%foreign "scheme:bitwise-and"
(.&.) : Int -> Int -> Int

infixl 8 .|.
export
%foreign "scheme:bitwise-ior"
(.|.) : Int -> Int -> Int

%foreign "scheme:bitwise-xor"
export
xor : Int -> Int -> Int

%foreign "scheme:bitwise-not"
export
not : Int -> Int

export
leadingBits : Bits8 -> Int
leadingBits b0 = count (cast b0) 7
  where
    count : Int -> Int -> Int
    count b p = if p >= 0 && b .&. shiftL 1 p > 0
                  then 1 + count b (p - 1)
                  else 0

-- Bits8 is always a valid codepoint
export
bits8ToChar : Bits8 -> Char
bits8ToChar = cast . cast {to=Int}

export
Range Char where
  rangeFromTo x y = cast <$> rangeFromTo {a=Int} (cast x) (cast y)
  rangeFromThenTo x y z
    = cast <$> rangeFromThenTo {a=Int} (cast x) (cast y) (cast z)
  rangeFrom x = cast <$> rangeFrom {a=Int} (cast x)
  rangeFromThen x y = cast <$> rangeFromThen {a=Int} (cast x) (cast y)


text:
-- USAGE: $ idris2 -q -x main shell-cmd.idr
-- BAD: shebang only supported by Idris1
--   https://github.com/idris-lang/Idris-dev/pull/2289
-- #!/usr/bin/env -S idris2 -q -x main

-- SRC: https://stackoverflow.com/questions/39812465/how-can-i-call-a-subprocess-in-idris

import System

main : IO ()
main = do
  exitCode <- system "echo HelloWorld!"
  putStrLn $ "Exit code: " ++ show exitCode

  exitCode <- system "echo HelloWorld!; false"
  putStrLn $ "Exit code: " ++ show exitCode

max_stars_repo_name: amerlyq/aeternum-langs

max_issues_repo_name: amerlyq/aeternum-langs

max_forks_repo_name: amerlyq/aeternum-langs


text:
-- vim: set ft=idris sw=2 ts=2:
--
-- benchmark.idr
-- A set of (micro-) benchmarks for the Idris programming language
--

module Main

import System
import Fibonacci
import PerfectNumber

-- convert list to string
show_list : Show a => List a -> String
show_list [] = ""
show_list (x :: xs) = (show x) ++ ", " ++ show_list xs

-- main entry point
main : IO ()
main = do
  tic <- System.time
  putStrLn $ "fib_naive(35) = " ++ (show (fib_naive 35))
  toc <- System.time
  putStrLn $ "Elapsed " ++ (show (toc - tic)) ++ "s."

  tic <- System.time
  putStrLn $ "fib(35) = " ++ (show (Fibonacci.fib 35))
  toc <- System.time
  putStrLn $ "Elapsed " ++ (show (toc - tic)) ++ "s."

  tic <- System.time
  putStrLn $ "fib(1000) = " ++ (show (Fibonacci.fib 1000))
  toc <- System.time
  putStrLn $ "Elapsed " ++ (show (toc - tic)) ++ "s."

  tic <- System.time
  putStrLn $ "pn(1000) = " ++ (show (perfect_numbers 1000))
  toc <- System.time
  putStrLn $ "Elapsed " ++ (show (toc - tic)) ++ "s."

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module System.File.Permissions

import public System.File.Error
import System.File.Support
import public System.File.Types

%default total

%foreign support "idris2_chmod"
         "node:support:chmod,support_system_file"
prim__chmod : String -> Int -> PrimIO Int

||| The UNIX file modes.
namespace FileMode
  public export
  data FileMode = Read | Write | Execute

||| The permissions of a file, grouped by the 3 types of owners of a file.
public export
record Permissions where
  constructor MkPermissions
  user   : List FileMode
  group  : List FileMode
  others : List FileMode

||| Convert the given `Permissions` to their integer value.
mkMode : Permissions -> Int
mkMode p
    = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
  where
    getM : FileMode -> Int
    getM Read = 4
    getM Write = 2
    getM Execute = 1

    getMs : List FileMode -> Int
    getMs = sum . map getM

||| Change the permissions of the file with the specified name to the given
||| integer representation of some permissions.
||| You likely want to use `chmod` and `Permissions`, or go via `mkMode`
||| instead of using this.
|||
||| @ fname the name of the file whose permissions to change
||| @ p     the integer representation of the permissions to set
export
chmodRaw : HasIO io => (fname : String) -> (p : Int) -> io (Either FileError ())
chmodRaw fname p
    = do ok <- primIO $ prim__chmod fname p
         if ok == 0
            then pure (Right ())
            else returnError

||| Change the permissions of the file with the specified name to the
||| permissions in the given `Permissions` record.
|||
||| @ fname the name of the file whose permissions to change
||| @ p     a `Permissions` record containing the permissions to set
export
chmod : HasIO io => (fname : String) -> (p : Permissions) -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p)


text:
module Main

import Data.Vect

factorialAux : Integer -> Integer -> Integer
factorialAux 0 a = a
factorialAux n a = factorialAux (n-1) (a*n)

factorial : Integer -> Integer
factorial n = factorialAux n 1

main : IO ()
main =
   do
      printLn $ factorial 100
      printLn $ factorial 10000
      printLn $ show $ the (Vect 3 String) ["red", "green", "blue"]


text:
module Arduino.Lib

import public Arduino.Boards
import Arduino.Raw
import public Arduino.Time
import public Arduino.Wrapper

%default total

-- Note: functions naming was left to be (at least for now) as they were at the the original Arduino software.

-- For now, this function is meant to be used only with digital pins.
-- Also, for now, it is using `IO` directly under the `Ard`.
export
pinMode : {board : Board} -> {auto hdp : HasDigitalPins board}
       -> (pin : Pin) -> {auto cbd : CanBeDigital {board} pin}
       -> (purpose : PinPurpose)
       -> Ard board (const Unit) (oneFact pin purpose) IO Unit
pinMode {board} {cbd} pin purpose = ard $ Arduino.Raw.pinMode (lowLevelNumberForDigitalPin {board} pin) (lowLevelNumberForPurpose purpose)
  where lowLevelNumberForPurpose : PinPurpose -> Bits8
        lowLevelNumberForPurpose Input  = 0
        lowLevelNumberForPurpose Output = 1

export
digitalWrite : {board : Board} -> {auto hdp : HasDigitalPins board}
            -> (pin : Pin) -> {auto cbd : CanBeDigital {board} pin}
            -> DigitalPinValue
            -> Ard board (LastFactEq pin Output) NoFacts IO Unit
digitalWrite {board} {cbd} pin value = ard $ Arduino.Raw.digitalWrite (lowLevelNumberForDigitalPin {board} pin) (lowLevelNumberForValue value)
  where lowLevelNumberForValue : DigitalPinValue -> Bits8
        lowLevelNumberForValue Low  = 0
        lowLevelNumberForValue High = 1

-- TODO To think, whether a time of the delay is a fact to represent at the typelevel or not.
export
sleepFor : {board : Board} -> Time -> Ard board (const Unit) NoFacts IO Unit
sleepFor = ard . Arduino.Time.sleepFor

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
data A = B | B

data C : Type -> Type where
  D : C Int
  D : C String


text:
module Compiler.Erlang.Name

import Data.List
import Core.Name
import Core.TT

%default total

public export
data OutputBundle : Type where
  Concat : (ns : String) -> OutputBundle
  Split : (prefixStr : String) -> (inNS : Namespace) -> OutputBundle

export
Eq OutputBundle where
  (Concat ns1) == (Concat ns2) = ns1 == ns2
  (Split prefix1 inNS1) == (Split prefix2 inNS2) = prefix1 == prefix2 && inNS1 == inNS2
  _ == _ = False

Ord OutputBundle where
  compare (Concat ns1) (Concat ns2) = compare ns1 ns2
  compare (Split prefix1 inNS1) (Split prefix2 inNS2) =
    case compare prefix1 prefix2 of
      LT => LT
      GT => GT
      EQ => compare inNS1 inNS2
  compare (Concat _) (Split _ _) = LT
  compare (Split _ _) (Concat _) = GT

public export
record NamespaceInfo where
  constructor MkNamespaceInfo
  outputBundle : OutputBundle

export
Eq NamespaceInfo where
  (MkNamespaceInfo outputBundle1) == (MkNamespaceInfo outputBundle2) =
    outputBundle1 == outputBundle2

export
Ord NamespaceInfo where
  compare (MkNamespaceInfo outputBundle1) (MkNamespaceInfo outputBundle2) =
    compare outputBundle1 outputBundle2

export
getNamespace : Name -> Namespace
getNamespace (NS ns _) = ns
getNamespace n = emptyNS -- TODO: Fix emptyNS

genName : Name -> String
genName (NS ns n) = "ns--" ++ show ns ++ "--" ++ genName n
genName (UN n) = "un--" ++ n
genName (MN n i) = n ++ "_" ++ show i
genName (PV n d) = "pat--" ++ genName n
genName (DN _ n) = "dn--" ++ genName n
genName (Nested (i, x) n) = "nested--" ++ show i ++ "-" ++ show x ++ "--in--" ++ genName n
genName (CaseBlock x y) = "case--" ++ x ++ "-" ++ show y
genName (WithBlock x y) = "with--" ++ x ++ "-" ++ show y
genName (Resolved i) = "fn--" ++ show i

moduleNameForNS : NamespaceInfo -> Namespace -> String
moduleNameForNS namespaceInfo ns =
  case outputBundle namespaceInfo of
    Concat ns => ns
    Split prefixStr inNS => show $ mkNamespace prefixStr <.> ns

moduleNameForName : NamespaceInfo -> Name -> String
moduleNameForName namespaceInfo name = moduleNameForNS namespaceInfo (getNamespace name)

export
currentModuleName : NamespaceInfo -> String
currentModuleName namespaceInfo =
  case outputBundle namespaceInfo of
    Concat ns => ns
    Split _ inNS => moduleNameForNS namespaceInfo inNS

export
isNameInCurrentModule : NamespaceInfo -> Name -> Bool
isNameInCurrentModule namespaceInfo name =
  case outputBundle namespaceInfo of
    Concat _ => True
    Split _ inNS => moduleNameForName namespaceInfo name == currentModuleName namespaceInfo

export
moduleNameFunctionName : NamespaceInfo -> Name -> (String, String)
moduleNameFunctionName namespaceInfo name =
  case outputBundle namespaceInfo of
    Concat ns => (ns, genName name)
    Split _ _ => (moduleNameForName namespaceInfo name, genName (dropNS name))

export
constructorName : Name -> String
constructorName name =
  let ns = mkNamespace "Idris" <.> getNamespace name
      ctorName = case dropNS name of
        (UN dataCtor) => dataCtor
        n => genName n
  in show ns ++ "." ++ ctorName

-- NAMESPACES

export
erlangTypesNS : Namespace
erlangTypesNS = mkNamespace "Erlang.Types"

export
erlangIONS : Namespace
erlangIONS = mkNamespace "Erlang.IO"

export
erlangMaybeImproperListNS : Namespace
erlangMaybeImproperListNS = mkNamespace "Erlang.Types.MaybeImproperList"

export
erlangProperListNS : Namespace
erlangProperListNS = mkNamespace "Erlang.Types.ProperList"


text:
module Mergesort

import Data.Vect

--Takes the first m elements from a vector
Vecttake : (m:Nat)->Vect n elem->Vect m  elem
Vecttake Z xs = []
Vecttake (S k) (x::xs) = x::(Vecttake k xs)
--Takes the last m elements from a vector
Vecttakefromlast :(m:Nat)->Vect n elem ->Vect m elem
Vecttakefromlast m xs = reverse (Vecttake  m (reverse xs))

insertend : (x:elem)->Vect n elem->Vect (S n) elem
insertend x [] = [x]
insertend x (y :: xs) = y::(insertend x xs)

--this function is to cast a vector from one type to another
sillycast: (v1:(Vect ((S k) + j) elem)) ->( Vect (k+ (S j)) elem)
sillycast {k} {j} v1 = (Vecttake k v1) ++(Vecttakefromlast (S j) v1)
--The merge function
merge1 :Ord elem =>Vect  n elem ->Vect  m elem ->Vect (n+m) elem
merge1 [] ys = ys
merge1  (x :: xs) [] =  (x::xs)++[]
merge1 {n= (S k)}{m= (S j)} (x :: xs) (y :: ys) = case x<=y of
                                 False => y::(sillycast( (merge1  (x::xs) ys)))
                                 True => x::(merge1 xs (y::ys))

{-mergesort :Ord elem=>Vect n elem->Vect n elem
mergesort []=[]
mergesort [x] = [x]
mergesort {n} xs = (the (Vect n elem ) (merge left right)) where
  left = mergesort (Vecttake s xs)
  right = mergesort (Vecttake (cast ((cast n)-(cast s))) xs) where
    s =cast((cast n)/2)-}


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module BareMetal.GPIO

import BareMetal.BitHandler
import BareMetal.SocAM335x
import BareMetal.HwCmPer
import BareMetal.HwGPIO

%access public export
%default total
%include C "bithandler.h"

gpioModuleClkConfig : Int -> IO ()
gpioModuleClkConfig gpioNum =
    let
        cmPerGpioClkctrl = cmPerGpio1Clkctrl
        cmPerGpioClkctrlIdlest = cmPerGpio1ClkctrlIdlest
        cmPerGpioClkctrlIdlestFunc = cmPerGpio1ClkctrlIdlestFunc
        cmPerGpioClkctrlIdlestShift = cmPerGpio1ClkctrlIdlestShift
        cmPerGpioClkctrlModulemode = cmPerGpio1ClkctrlModulemode
        cmPerGpioClkctrlModulemodeEnable = cmPerGpio1ClkctrlModulemodeEnable
        cmPerGpioClkctrlOptfclkenGpioGdbclk = cmPerGpio1ClkctrlOptfclkenGpio1Gdbclk
        cmPerL4lsClkstctrlClkactivityGpioGdbclk = cmPerL4lsClkstctrlClkactivityGpio1Gdbclk
    in
        do
            writeAddrWaitMask
                (socCmPerRegs + cmPerGpioClkctrl)
                cmPerGpioClkctrlModulemodeEnable
                cmPerGpioClkctrlModulemode
            writeAddrWait
                (socCmPerRegs + cmPerGpioClkctrl)
                cmPerGpioClkctrlOptfclkenGpioGdbclk
            addrWaitMask
                (socCmPerRegs + cmPerGpioClkctrl)
                0
                cmPerGpioClkctrlIdlest
            addrWaitMask
                (socCmPerRegs + cmPerL4lsClkctrl)
                cmPerL4lsClkstctrlClkactivityGpioGdbclk
                cmPerL4lsClkstctrlClkactivityGpioGdbclk

gpio1Pin23PinMuxSetup : IO ()
gpio1Pin23PinMuxSetup =
    let
        addr = socControlRegs + 0x840 + (7 * 4)
        val = 7
    in
        writeAddrWait addr val

gpioModuleEnable : Bits32 -> IO ()
gpioModuleEnable baseAddr =
    addrClearBits
        (baseAddr + gpioCtrl)
        gpioCtrlDisablemodule

gpioModuleReset : Bits32 -> IO ()
gpioModuleReset baseAddr = do
    addrSetBits
        (baseAddr + gpioSysconfig)
        gpioSysconfigSoftreset
    addrWaitMask
        (baseAddr + gpioSysstatus)
        0
        gpioSysstatusResetdone

gpioDirModeSet : Bits32 -> Int -> Bool -> IO ()
gpioDirModeSet baseAddr pinNumber outDirection =
    let
       addr = baseAddr + gpioOe
       mask = Prelude.pow 2 $ toNat pinNumber
       func =
           if outDirection
              then addrClearBits
              else addrSetBits
    in func addr mask

gpioPinWrite : Bits32 -> Int -> Bool -> IO ()
gpioPinWrite baseAddr pinNumber pinHigh =
    let
        val = Prelude.pow 2 $ toNat pinNumber
        addr = baseAddr +
            if pinHigh
                then gpioSetdataout
                else gpioCleardataout
    in
        writeAddrWait addr val

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
module Greet

%default total

data InfIO : Type where
     Do : IO a ->
          (a -> Inf InfIO) ->
          InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

greet : InfIO
greet = do putStr "Enter thy name: "
           name <- getLine
           putStrLn ("Howdy " ++ name)
           greet

max_stars_repo_path: Chapter 11/Greet.idr

max_issues_repo_path: Chapter 11/Greet.idr

max_forks_repo_path: Chapter 11/Greet.idr


text:
module Core.FC

import Text.PrettyPrint.Prettyprinter

%default total

public export
FilePos : Type
FilePos = (Int, Int)

showPos : FilePos -> String
showPos (l, c) = show (l + 1) ++ ":" ++ show (c + 1)

public export
FileName : Type
FileName = String

||| A file context is a filename together with starting and ending positions
public export
data FC = MkFC FileName FilePos FilePos
        | EmptyFC

export
Eq FC where
  (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
  (==) EmptyFC EmptyFC = True
  (==) _ _ = False

export
file : FC -> FileName
file (MkFC fn _ _) = fn
file EmptyFC = ""

export
startPos : FC -> FilePos
startPos (MkFC _ s _) = s
startPos EmptyFC = (0, 0)

export
endPos : FC -> FilePos
endPos (MkFC _ _ e) = e
endPos EmptyFC = (0, 0)

-- Return whether a given file position is within the file context (assuming we're
-- in the right file)
export
within : FilePos -> FC -> Bool
within (x, y) (MkFC _ start end)
   = (x, y) >= start && (x, y) <= end
within _ _ = False

-- Return whether a given line is on the same line as the file context (assuming
-- we're in the right file)
export
onLine : Int -> FC -> Bool
onLine x (MkFC _ start end)
   = x >= fst start && x <= fst end
onLine _ _ = False

export
emptyFC : FC
emptyFC = EmptyFC

export
toplevelFC : FC
toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)

%name FC fc

export
Show FC where
  show loc = file loc ++ ":" ++
             showPos (startPos loc) ++ "--" ++
             showPos (endPos loc)

export
Pretty FC where
  pretty loc = pretty (file loc) <+> colon
                 <+> prettyPos (startPos loc) <+> pretty "--"
                 <+> prettyPos (endPos loc)
    where
      prettyPos : FilePos -> Doc ann
      prettyPos (l, c) = pretty (l + 1) <+> colon <+> pretty (c + 1)


text:
import Data.Vect
import Data.IORef
import Data.IOArray
import Data.String
import Data.Vect
import Data.List
import System
data MyData = MyCons0 Nat | MyCons1

Show MyData where
  show (MyCons0 x) = "blah" ++ show x
  show MyCons1 = "babah"

boom : Nat -> Nat
boom (S k) = boom k
boom Z = 32

whatData : MyData -> Nat
whatData (MyCons0 x) = x
whatData MyCons1 = 99

factorial : Integer -> Integer -> Integer
factorial 0 ac = ac
factorial x ac = factorial (x - 1) (ac * x)

data BTree a = BBranch (BTree a) a (BTree a) | BLeaf

intPow : Integer -> Integer -> Integer
intPow base exp =
  if exp > 1 then base * (intPow base (exp - 1)) else if exp == 1 then base else 1

fillIn : Nat -> List Nat -> (Nat -> Nat -> a) -> BTree a
fillIn Z _ f = BLeaf
fillIn (S k) l f =
  BBranch
   (fillIn k (0 :: l) f)
    (f k $ count k (reverse l))
     (fillIn k (1 :: l) f)
where
  count : Nat -> List Nat -> Nat
  count k (x :: xs) = let len = length xs in x * (integerToNat $ intPow 2 (cast len)) + count k xs
  count _ [] = 0

printLeft : Show a => BTree a -> String
printLeft BLeaf = ""
printLeft (BBranch l x r) = printLeft l ++ " " ++ show x ++ " " ++ printLeft r

indent : Nat -> String
indent k = pack $ replicate (2 * k) ' '

Cast Nat String where
  cast x = cast $ cast {to = Int} x

testInteger : Integer -> Integer -> Integer
testInteger x y = x * x * x * x - 1

%hide Prelude.print

data Lua : Type where [external]

%foreign "lua:function (_) return function (x) return idris.inspect(x) end end|inspect"
inspect : (x : a) -> String

%foreign "lua:function(x) return function (str) return x[str] end end|inspect"
dot : Lua -> String -> Lua

%foreign "lua:function (x) return require (x) end"
require : String -> Lua

%foreign "lua:function(a) return function(b) return function(f) return function(x) return f(x) end end end end"
call : {0 a : Type} -> {0 b : Type} -> Lua -> a -> b

%foreign "lua:print"
print_ : String -> ()

print : (HasIO io) => String -> io ()
print x = pure $ print_ x

main : IO ()
main = do
  let ins = require "inspect"
  putStrLn $ call (ins `dot` "inspect") [1, 2, the Int 3] {a = List _} {b = String}

  v <- newIORef ""
  print "enter something:"
  writeIORef v !(getLine)
  print $ "you said " ++ !(readIORef v)
  putStrLn $ if 1 > 2 then "not ok" else "ok"
  printLn $ (the Int 1)
  putStrLn $ show (the Nat 28)
  putStrLn $ show $ whatData $ MyCons0 7
  ar <- newArray 10 {elem = Int}
  pure ()
  let from = the Int (fromInteger 10)
  putStrLn $ show $ "ok " ++ "or not"
  putStrLn $ show (5 == the Int 5)
  putStrLn $ show (0 == the Integer 0)
  putStrLn $ show (1 < the Integer 2)
  putStrLn $ show (7 < the Int 4)
  args <- getArgs
  traverse_ putStrLn args

  putStrLn $ show $ (the Integer 0) > 0
  putStrLn $ show $ testInteger 2 5
  putStrLn $ "2 ^ 6 == " ++ show (intPow 2 6)
  let  tr = fillIn 4 [] (\d, i => show d ++ " " ++ show i)
  putStrLn $ printLeft tr

  putStrLn $ "the guts of BTree look like this: " ++ inspect tr

  putStrLn $ show from
  putStrLn $ show $ (the Integer (2 - 2)) == 0
  putStrLn $ show $ factorial 1000 1
  putStrLn "unicode string: lambda λ, sigma Σ, integral ∫, cyrillic F Ф"


text:
module Main

import Control.App
import Control.App.Console

data Counter : Type where

--helloCount : (Console es, State Counter Int es) => App es ()
helloCount : Has [Console, State Counter Int] es => App es ()
helloCount = do c <- get Counter
                put Counter (c + 1)
                putStrLn "Hello, counting world!"
                c <- get Counter
                putStrLn $ "Counter: " ++ show c

main : IO ()
main = run (new 93 helloCount)

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Graphiti.BTree

-- shows a basic Binary Tree with insert, toList and fromList ops
-- shows how to reverse/invert it without using a stack or a queue

%hide toList -- we do not want the standard library to pollute our definitions here

public export
data BTree a = Leaf | Node (BTree a) a (BTree a)

data LR = L | R

inserter : Ord a => a ->  BTree a -> LR -> BTree a
inserter x Leaf _ = Node Leaf x Leaf
inserter x (Node l y r) L = if (x < y) then (Node (inserter x l L) y r)
                                    else (Node l y (inserter x r L))
inserter x (Node l y r) R = if (x > y) then (Node (inserter x l R) y r)
                                    else (Node l y (inserter x r R))

export
insert : Ord a => a -> BTree a -> BTree a
insert x t = inserter x t L

invInsert : Ord a => a -> BTree a -> BTree a
invInsert x t = inserter x t R

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l y r) = BTree.toList l ++ (y :: BTree.toList r)

export
fromList : Ord a => List a -> BTree a
fromList [] = Leaf
fromList (x :: xs) = BTree.insert x (BTree.fromList xs)

fromListInv : Ord a => List a -> BTree a
fromListInv [] = Leaf
fromListInv (x :: xs) = invInsert x (fromListInv xs)

export
reverseList : List a -> List a
reverseList xs = revAcc [] xs where
    revAcc : List a -> List a -> List a
    revAcc acc [] = acc
    revAcc acc (y :: ys) = revAcc (y :: acc) ys

export
revBTree : Ord a => BTree a -> BTree a
revBTree Leaf = Leaf
revBTree node = fromList ( BTree.reverseList (BTree.toList node) )

export
reinvBTree : Ord a => BTree a -> BTree a
reinvBTree Leaf = Leaf
reinvBTree node = fromListInv (toList node)

-- shows a proof that inversion of inversion is the original
-- i.e. inv . inv = id

invOfInv : Ord a => (bt: BTree a) -> reinvBTree (reinvBTree bt) = bt
invOfInv Leaf = Refl
invOfInv (Node x y z) = ?hole

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti